A:Type, eq:EqDecider(A), B:(AType), P:(A), f:x:A fp B(x), x:{a:A| P(a) }, v:B(x).
(<x,v>  fpf-vals(eq;P;f))  {x  dom(f) & v = f(x)} 

latex

Definitions	x:AB(x), P  Q, x:AB(x), P & Q, P  Q, t  T, x:A. B(x), b, x(s), Type, EqDecider(T), , f(a), x. t(x), a:A fp B(a), {x:A| B(x) }, x.A(x), fpf-vals(eq;P;f), <a,b>, (x  l), s = t, {T}, S  T
Lemmas	l member subtype, l member wf, fpf-vals wf, assert wf, fpf wf, bool wf, deq wf, member-fpf-vals